Nuprl Lemma : void-list-equality2
0,22
postcript
pdf
x
,
y
:Void List,
T
:Type.
x
=
y
T
List
latex
Definitions
Void
,
t
T
,
type
List
,
Type
,
s
=
t
,
x
:
A
.
B
(
x
)
,
s
~
t
,
x
:
A
B
(
x
)
,
S
T
Lemmas
void-list-equality
origin
x, y:Void List, T:Type. x = y 
T List x, y:Void List, T:Type. x = y T List Tx:A. B(x)
B(x)
T